﻿/*============================================
 * 类名 :CreateProcess
 * 描述 :根据树形的推理过程，得到正规的离散数学表示形式
 *   
 * 创建时间: 2011-2-1 19:05:43
 * Blog:   http://home.cnblogs.com/xiangism
 *============================================*/
using System;
using System.Collections.Generic;
using System.Text;

namespace 命题证明
{
    /// <summary>根据树形的推理过程，得到正规的离散数学表示形式</summary>
    class CreateProveProcess
    {
        public CreateProveProcess()
        {
            List<bool> t = new List<bool>() { false };
            graph.Add( t );
        }

        List<ResultParameter> result = new List<ResultParameter>();
        List<ProveNode> nodes = new List<ProveNode>();
        List<int> outed = new List<int>();
        List<List<bool>> graph = new List<List<bool>>();

        /// <summary>创建最后的证明过程</summary>
        public List<ResultParameter> CreateProcess( ProveNode node )
        {
            CreateGraph( node );
            while ( outed.Count != nodes.Count )
            {
                int t = FindLast();
                List<int> p = new List<int>();
                //nodes[t].Previous.ForEach( delegate( ProveNode n ) {
                //    p.Add( FindPrevious( n ) );
                //} );

                for ( int i = 0; i < nodes[t].Previous.Count; i++ )
                {

                    p.Add( FindPrevious( nodes[t].Previous[i] ) );

                }

                ResultParameter r = new ResultParameter(nodes[t].Result.ToString(),  nodes[t].ProveName );
                r.Previous = p;
                //r.LawName = ;
                //r.Content = ;
                result.Add( r );
                outed.Add( t );
            }
            return result;
        }
        int FindPrevious( ProveNode n )
        {
            for ( int i = 0; i < result.Count; i++ )
            {
                if ( result[i].Content == n.Result.ToString() )
                    return i;
            }
            throw new Exception( "在生成最后的证明过程时，出现了不可能出现的错误" );
        }

        private int FindLast()
        {
            for ( int i = 0; i < graph.Count; i++ )
            {
                if ( IsExist( i ) && IsAllFalse( i ) )
                    return i;
            }
            throw new Exception( "在拓扑排序时找不到最后一个节点" );
        }

        private bool IsAllFalse( int i )
        {
            for ( int j = 0; j < graph[i].Count; j++ )
            {
                if ( IsExist( j ) && graph[i][j] )
                    return false;
            }
            return true;
        }

        bool IsExist( int index )
        {
            for ( int i = 0; i < outed.Count; i++ )
            {
                if ( outed[i] == index )
                    return false;
            }
            return true;
        }

        void CreateGraph( ProveNode value )
        {
            for ( int i = 0; i < value.Previous.Count; i++ )
            {
                AddNode( value, value.Previous[i] );
                CreateGraph( value.Previous[i] );
            }
        }

        private void AddNode( ProveNode value, ProveNode next )
        {
            int fromIndex = GetIndex( value );
            int toIndex = GetIndex( next );
            SetGraph( fromIndex, toIndex );
        }

        private void SetGraph( int from, int next )
        {
            int max = from > next ? from : next;
            if ( max == graph.Count )
            {
                for ( int i = 0; i < graph.Count; i++ )
                {
                    graph[i].Add( false );
                }
                List<bool> add = new List<bool>();
                for ( int i = 0; i <= max; i++ )
                {
                    add.Add( false );
                }
                graph.Add( add );
            }
            graph[from][next] = true;
        }

        int GetIndex( ProveNode value )
        {
            for ( int i = 0; i < nodes.Count; i++ )
            {
                if ( value == nodes[i] )
                {
                    return i;
                }
            }
            nodes.Add( value );
            return nodes.Count - 1;
        }

    }

}
